# HG changeset patch # User wenzelm # Date 1001598128 -7200 # Node ID d8a7f6318457b8c4f7fbb3241cf62eac7f3bdbcd # Parent 35a79fd062f7d20ad4d66d5a8def8bb26f68cc74 tuned; diff -r 35a79fd062f7 -r d8a7f6318457 src/HOL/ex/Antiquote.thy --- a/src/HOL/ex/Antiquote.thy Thu Sep 27 15:42:01 2001 +0200 +++ b/src/HOL/ex/Antiquote.thy Thu Sep 27 15:42:08 2001 +0200 @@ -2,14 +2,17 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen License: GPL (GNU GENERAL PUBLIC LICENSE) - -Simple quote / antiquote example. *) header {* Antiquotations *} theory Antiquote = Main: +text {* + A simple example on quote / antiquote in higher-order abstract + syntax. +*} + syntax "_Expr" :: "'a => 'a" ("EXPR _" [1000] 999) @@ -35,4 +38,3 @@ term "Expr (\env. f env + g env y + h a env z)" end - diff -r 35a79fd062f7 -r d8a7f6318457 src/HOL/ex/Multiquote.thy --- a/src/HOL/ex/Multiquote.thy Thu Sep 27 15:42:01 2001 +0200 +++ b/src/HOL/ex/Multiquote.thy Thu Sep 27 15:42:08 2001 +0200 @@ -2,15 +2,17 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen License: GPL (GNU GENERAL PUBLIC LICENSE) - -Multiple nested quotations and anti-quotations -- basically a -generalized version of de-Bruijn representation. *) header {* Multiple nested quotations and anti-quotations *} theory Multiquote = Main: +text {* + Multiple nested quotations and anti-quotations -- basically a + generalized version of de-Bruijn representation. +*} + syntax "_quote" :: "'b => ('a => 'b)" (".'(_')." [0] 1000) "_antiquote" :: "('a => 'b) => 'b" ("\_" [1000] 1000) diff -r 35a79fd062f7 -r d8a7f6318457 src/HOL/ex/NatSum.thy --- a/src/HOL/ex/NatSum.thy Thu Sep 27 15:42:01 2001 +0200 +++ b/src/HOL/ex/NatSum.thy Thu Sep 27 15:42:08 2001 +0200 @@ -36,7 +36,8 @@ *} lemma sum_of_odd_squares: - "#3 * setsum (\i. Suc (i + i) * Suc (i + i)) (lessThan n) = n * (#4 * n * n - #1)" + "#3 * setsum (\i. Suc (i + i) * Suc (i + i)) (lessThan n) = + n * (#4 * n * n - #1)" apply (induct n) txt {* This removes the @{term "-#1"} from the inductive step *} apply (case_tac [2] n) @@ -61,17 +62,20 @@ \medskip The sum of the first @{term n} positive integers equals @{text "n (n + 1) / 2"}.*} -lemma sum_of_naturals: "#2 * setsum id (atMost n) = n * Suc n" +lemma sum_of_naturals: + "#2 * setsum id (atMost n) = n * Suc n" apply (induct n) apply auto done -lemma sum_of_squares: "#6 * setsum (\i. i * i) (atMost n) = n * Suc n * Suc (#2 * n)" +lemma sum_of_squares: + "#6 * setsum (\i. i * i) (atMost n) = n * Suc n * Suc (#2 * n)" apply (induct n) apply auto done -lemma sum_of_cubes: "#4 * setsum (\i. i * i * i) (atMost n) = n * n * Suc n * Suc n" +lemma sum_of_cubes: + "#4 * setsum (\i. i * i * i) (atMost n) = n * n * Suc n * Suc n" apply (induct n) apply auto done diff -r 35a79fd062f7 -r d8a7f6318457 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Thu Sep 27 15:42:01 2001 +0200 +++ b/src/HOL/ex/ROOT.ML Thu Sep 27 15:42:08 2001 +0200 @@ -8,6 +8,20 @@ time_use_thy "Recdefs"; time_use_thy "Primrec"; +setmp proofs 2 time_use_thy "Hilbert_Classical"; + +(*advanced concrete syntax*) +time_use_thy "Tuple"; +time_use_thy "Antiquote"; +time_use_thy "Multiquote"; + +(*basic use of extensible records*) +time_use_thy "MonoidGroup"; +time_use_thy "Records"; + +time_use_thy "StringEx"; +time_use_thy "BinEx"; + time_use_thy "NatSum"; time_use "cla.ML"; time_use "mesontest.ML"; @@ -24,16 +38,4 @@ time_use_thy "MT"; time_use_thy "Tarski"; -time_use_thy "StringEx"; -time_use_thy "BinEx"; - if_svc_enabled time_use_thy "svc_test"; - -(*basic use of extensible records*) -time_use_thy "MonoidGroup"; -time_use_thy "Records"; - -(*advanced concrete syntax*) -time_use_thy "Tuple"; -time_use_thy "Antiquote"; -time_use_thy "Multiquote"; diff -r 35a79fd062f7 -r d8a7f6318457 src/HOL/ex/StringEx.thy --- a/src/HOL/ex/StringEx.thy Thu Sep 27 15:42:01 2001 +0200 +++ b/src/HOL/ex/StringEx.thy Thu Sep 27 15:42:08 2001 +0200 @@ -15,7 +15,8 @@ lemma "''ABCD'' = ''ABCD''" by simp -lemma "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' \ ''ABCDEFGHIJKLMNOPQRSTUVWXY''" +lemma "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' \ + ''ABCDEFGHIJKLMNOPQRSTUVWXY''" by simp lemma "set ''Foobar'' = {CHR ''F'', CHR ''a'', CHR ''b'', CHR ''o'', CHR ''r''}" diff -r 35a79fd062f7 -r d8a7f6318457 src/HOL/ex/mesontest2.thy --- a/src/HOL/ex/mesontest2.thy Thu Sep 27 15:42:01 2001 +0200 +++ b/src/HOL/ex/mesontest2.thy Thu Sep 27 15:42:08 2001 +0200 @@ -1,8 +1,7 @@ -(*Theory Product_Type instead of HOL regards arguments as tuples. - But theory Main would allow clashes with many other constants.*) +header {* Meson test cases *} -theory mesontest2 = Product_Type: +theory mesontest2 = Main: hide const inverse divide