git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@14190 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@14189 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@14185 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@14183 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@14004 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13997 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13995 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13993 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13991 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13987 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13986 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13985 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13984 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13983 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13982 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13981 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13772 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13768 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13763 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13536 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13534 3260e6d1-4efc-4170-b0a7-36055960796d

implement meta_command', similar as meta_command but providing the current computed state of the manipulated environment


git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13533 3260e6d1-4efc-4170-b0a7-36055960796d

display the immediate-level commands to be executed whenever meta_command receives native Isabelle commands in deep-mode


git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13532 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13531 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13513 3260e6d1-4efc-4170-b0a7-36055960796d

add an option to specify if the code generated by 'language' should be understood as being a generator of meta-commands, and then automatically executed in the latter case


git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13502 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13501 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13500 3260e6d1-4efc-4170-b0a7-36055960796d

generalize the folding from Core.thy to later theories, so that for instance all_meta_trs can be called in all_meta_tr whenever it would be needed for a command to recursively generate several meta-commands


git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13499 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13498 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13497 3260e6d1-4efc-4170-b0a7-36055960796d

fix r13210 : choosing a command_keyword classified as 'diag' would let the evaluating engine not propagate 'theory' results sequentially (which is necessary as Toplevel.read_write can be seen as acting on 'theory'). Then a solution is to use instead a 'thy_decl' tag.


git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13451 3260e6d1-4efc-4170-b0a7-36055960796d

fix r13210 : choosing a command_keyword classified as 'diag' would let the evaluating engine not propagate 'theory' results sequentially (which is necessary as Toplevel.read_write can be seen as acting on 'theory'). Then a solution is to use instead a 'thy_decl' tag.


git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13450 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13449 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13404 3260e6d1-4efc-4170-b0a7-36055960796d

git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13400 3260e6d1-4efc-4170-b0a7-36055960796d