| author | wneuper <Walther.Neuper@jku.at> |
| Thu, 20 Oct 2022 10:23:38 +0200 | |
| changeset 60571 | 19a172de0bb5 |
| parent 60217 | 1d9fee958a46 |
| child 60576 | 11dd56e2a6b8 |
| permissions | -rw-r--r-- |
| wneuper@59119 | 1 |
(* use this theory for tests before Build_Isac.thy has succeeded *) |
| wenzelm@60192 | 2 |
theory Test_Theory imports "$ISABELLE_ISAC/Specify/Specify" |
| neuper@52102 | 3 |
begin |
| wenzelm@60192 | 4 |
ML_file "$ISABELLE_ISAC/BaseDefinitions/libraryC.sml" |
| Walther@60571 | 5 |
(* ATTENTION: tests with Test_Code.init_calc, CalcTree @{context} do NOT work here, because Thy_Info.get_theory
|
| wenzelm@60217 | 6 |
requires session Isac, see $ISABELLE_ISAC_TEST/Tools/isac/ADDTESTS/session-get_theory *) |
| neuper@52102 | 7 |
|
| wneuper@59472 | 8 |
section \<open>code for copy & paste ===============================================================\<close> |
| wneuper@59472 | 9 |
ML \<open> |
| walther@59686 | 10 |
"~~~~~ fun xxx , args:"; val () = (); |
| walther@59686 | 11 |
"~~~~~ and xxx , args:"; val () = (); |
| walther@59723 | 12 |
"~~~~~ from fun xxx\<longrightarrow>fun yyy\<longrightarrow>fun zzz, return val:"; val () = (); |
| walther@59686 | 13 |
(*if*) (*then*); (*else*); (*case*) (*of*); (*return value*); |
| walther@59686 | 14 |
"xx" |
| walther@59686 | 15 |
^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*) |
| walther@59686 | 16 |
\<close> ML \<open> |
| wneuper@59472 | 17 |
\<close> |
| walther@59723 | 18 |
ML \<open> |
| walther@59723 | 19 |
\<close> ML \<open> |
| walther@59723 | 20 |
\<close> ML \<open> |
| walther@59723 | 21 |
\<close> |
| wneuper@59472 | 22 |
text \<open> |
| neuper@52102 | 23 |
declare [[show_types]] |
| neuper@52102 | 24 |
declare [[show_sorts]] |
| neuper@52102 | 25 |
find_theorems "?a <= ?a" |
| neuper@52102 | 26 |
|
| neuper@52102 | 27 |
print_facts |
| neuper@52102 | 28 |
print_statement "" |
| neuper@52102 | 29 |
print_theory |
| wneuper@59472 | 30 |
\<close> |
| wneuper@59472 | 31 |
ML \<open> |
| neuper@52102 | 32 |
(*========== inhibit exn WN130909 TODO ========================================================= |
| neuper@52102 | 33 |
============ inhibit exn WN130909 TODO ========================================================*) |
| neuper@52102 | 34 |
(*-.-.-.-.-. isolate response ad-hoc .-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
| neuper@52102 | 35 |
-.-.-.-.-.-. isolate response ad-hoc .-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*) |
| wneuper@59472 | 36 |
\<close> |
| neuper@52102 | 37 |
|
| wneuper@59472 | 38 |
section \<open>=================================================================\<close> |
| wneuper@59472 | 39 |
ML \<open> |
| wneuper@59472 | 40 |
\<close> ML \<open> |
| wneuper@59472 | 41 |
\<close> ML \<open> |
| wneuper@59472 | 42 |
\<close> ML \<open> |
| wneuper@59472 | 43 |
\<close> ML \<open> |
| wneuper@59472 | 44 |
\<close> ML \<open> |
| wneuper@59472 | 45 |
\<close> ML \<open> |
| wneuper@59472 | 46 |
\<close> |
| walther@60152 | 47 |
|
| wneuper@59472 | 48 |
section \<open>=================================================================\<close> |
| wneuper@59472 | 49 |
ML \<open> |
| wneuper@59472 | 50 |
\<close> ML \<open> |
| wneuper@59472 | 51 |
\<close> ML \<open> |
| wneuper@59472 | 52 |
\<close> ML \<open> |
| wneuper@59472 | 53 |
\<close> ML \<open> |
| wneuper@59472 | 54 |
\<close> ML \<open> |
| wneuper@59472 | 55 |
\<close> ML \<open> |
| wneuper@59472 | 56 |
\<close> |
| walther@60152 | 57 |
|
| wneuper@59472 | 58 |
section \<open>=================================================================\<close> |
| wneuper@59472 | 59 |
ML \<open> |
| wneuper@59472 | 60 |
\<close> ML \<open> |
| wneuper@59472 | 61 |
\<close> ML \<open> |
| wneuper@59472 | 62 |
\<close> ML \<open> |
| wneuper@59472 | 63 |
\<close> ML \<open> |
| wneuper@59472 | 64 |
\<close> ML \<open> |
| wneuper@59472 | 65 |
\<close> ML \<open> |
| wneuper@59472 | 66 |
\<close> ML \<open> |
| wneuper@59472 | 67 |
\<close> |
| neuper@52102 | 68 |
|
| neuper@52102 | 69 |
end |
| neuper@52102 | 70 |
|
| neuper@52102 | 71 |